Rinit{-}discrete($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case Rinit{-}v($A$) of inl($v$) =$>$ tt $\mid$ inr($v$) =$>$ ff